Nuprl Lemma : assert-q_le
11,40
postcript
pdf
a
,
b
:
. (
q_le(
a
;
b
)) ~
a
b
latex
Definitions
t
T
,
t
.2
,
t
.1
,
,
x
f
y
,
<
+>
,
a
b
,
r
s
,
q_le(
r
;
s
)
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
origin
a, b:
. (
q_le(a;b)) ~ a 
b a, b:. (q_le(a;b)) ~ a b 
T
+> b sx:A. B(x)